﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using Formality.FormalSystem;
using Formality.FormalSystem.Parser;
using Formality.FormalSystem.Reasoning;
using Formality.Game;
using Formality.Game.Database;
using Core;

namespace ProofChecker
{
    public class Program
    {
        public static void Main(string[] args)
        {
            if (args.Length == 2 && args[0] == "--load")
                Load(args[1]);

            var Checker = new ProofChecker<Proposition>("Blake", ParsingExtension.Parse, Check, true);

            if (!Checker.Check())
            {
                foreach (var Bad in Checker.Failures)
                    Console.WriteLine("Failed to prove " + Bad);

                throw new Exception("Some of the proofs were invalid");
            }
        }

        private static bool Check(Proposition g, IEnumerable<Sentence<Proposition>> Premises)
        {
            var PArray = (from p in Premises
                          select Tuple.New(p.Item, p.Id == null)).
                          ToArray();

            var Justification = g.Follows(PArray);

#if false
                if (Justification != null)
                {
                    Console.WriteLine("Allowing {0} because {1}", g,
                                      Justification.Name);
                }
                else
                {
                    Console.WriteLine("Rejecting " + g);
                }
#endif

            return Justification != null;
        }

        private static void Load(string Filename)
        {
            using (var Stream = File.Open(Filename, FileMode.Open))
            using (var Reader = new StreamReader(Stream))
            {
                var Lines = from Line in Reader.Lines()
                            select Line.Split(',');

                var Submissions = from Line in Lines
                                  select new
                                             {
                                                 Name = Line[0],
                                                 ProblemId = Line[1],
                                                 SubmissionOrder = Line[2],
                                                 Proposition = Line[3]
                                             };

                foreach (var Sub in Submissions)
                    @"  insert into submissions (PlayerId, ProblemId, SubmissionOrder, Proposition)
                        select PlayerId, @ProblemId, @SubmissionOrder, @Proposition
                        from Players
                        where Name=@Name"
                        .Execute(Sub);
            }
        }
    }

    internal static class StreamExt
    {
        public static IEnumerable<String> Lines(this TextReader Reader)
        {
            string Line;
            while ((Line = Reader.ReadLine()) != null)
                yield return Line;
        }
    }
}